Nuprl Lemma : null_append
11,40
postcript
pdf
T
:Type,
L1
,
L2
:(
T
List). null(
L1
@
L2
) ~ (null(
L1
)
null(
L2
))
latex
Definitions
t
T
,
if
b
then
t
else
f
fi
,
ff
,
tt
,
Y
,
p
q
,
as
@
bs
,
null(
as
)
,
x
:
A
.
B
(
x
)
origin
T:Type, L1, L2:(T List). null(L1 @ L2) ~ (null(L1) 
null(L2)) T:Type, L1, L2:(T List). null(L1 @ L2) ~ (null(L1) null(L2)) 
T qx:A. B(x)